$\forall$$x$:chain\_config(). ($\uparrow$ccpred?($x$)) $\Rightarrow$ (ccpred{-}id($x$) $\in$ Id)